// SPDX-License-Identifier: GPL-2.0 or GPL-3.0
// Copyright © 2019 Ariadne Devos

#ifndef _sHT_MATH_EXPNAT_POWER16_H
#define _sHT_MATH_EXPNAT_POWER16_H

#include <sHT/math/expnat.h>

// Desc: numeric values of common powers of 16
//   > Useful for overflow checking.
//   > These take a little computative effort.
// Proof status: auto
/*@ axiomatic Exp16 {
      // UINT8_MAX (if that were defined)
      lemma exp16_2: expnat(16, 2) == 0x100;
      // UINT16_MAX + 1
      lemma exp16_4: expnat(16, 4) == 0x10000;
      // UINT32_MAX + 1
      lemma exp16_8: expnat(16, 8) == 0x100000000;
    } */

#endif
